COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDCONST WISE1 WISE2 WISE3 ε PERSON
C00003 ENDMK
C⊗;
DECLARE INDCONST WISE1 WISE2 WISE3 ε PERSON;
DECLARE INDCONST RW ε WORLD;
DECLARE INDCONST WHITE1 WHITE2 WHITE3 εPROPOSITION;

AXIOM WISEMAN:
	T(WHITE1,RW)∧T(WHITE2,RW)∧T(WHITE3,RW),
	T(K(FOOL,KW(WISE1,WHITE2)),RW),
	T(K(FOOL,KW(WISE1,WHITE3)),RW),
	T(K(FOOL,KW(WISE2,WHITE1)),RW),
	T(K(FOOL,KW(WISE2,WHITE3)),RW),
	T(K(FOOL,KW(WISE3,WHITE1)),RW),
	T(K(FOOL,KW(WISE3,WHITE2)),RW),
	T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW),

	T(K(WISE3,K(WISE2,NOT(K(WISE1,WHITE1)))),RW),
	T(K(WISE3,NOT(K(WISE2,WHITE2))),RW);
;